Section: Software and Platforms

Aspic

Participant : Laure Gonnord.

Aspic is an invariant generator for general counter automata. Used with C2fsm (see Section  5.10 ), it can be used to derivate invariant for numerical C programs, and also prove safety. It is also part of the WTC toolsuite (see http://compsys-tools.ens-lyon.fr/wtc/index.html ), a set of examples to demonstrate the capability of the RanK tool (see Section  5.12 ) for evaluating worse-case time complexity (number of transitions when executing an automaton).

Aspic implements the theoretical results of Laure Gonnord's PhD thesis on acceleration techniques and has been maintained since 2007.